T, T':Type, a:T List, f, g:(TT').
(x:T. (x  a)  f(x) = g(x))  map(f;a) = map(g;a)  T' List 

latex

Definitions	t  T, x:A. B(x), A List, Prop, (x  l), P  Q, ||as||, i<j, b, False, A, AB, ij, P  Q, P & Q, P  Q, True, T,
Lemmas	listp properties, bool wf, squash wf, true wf, map length, assert of lt int, map equal2, assert wf, lt int wf, length wf1, l member wf, listp wf